
@manuscript{Abadi:93,
title={{Types for the Scott Numerals}},
author={M. Abadi and L. Cardelli and G. Plotkin},
note="Unpublished, available from Abadi's web page",
year=1993,
pages={1--2}}                  

@techreport{mendler:1987,
  title={Inductive definition in type theory},
  author={P. Mendler},
  year={1987},
  institution={Cornell University}
}
@techreport{coquand:inria-00075471,
    hal_id = {inria-00075471},
    url = {http://hal.inria.fr/inria-00075471},
    title = {{Metamathematical investigations of a calculus of constructions}},
    author = {T. Coquand},
    language = {English},
    affiliation = {INRIA Rocquencourt - INRIA Rocquencourt},
    institution = {INRIA},
    number = {RR-1088},
    year = {1989},
    month = Sep,
    pdf = {http://hal.inria.fr/inria-00075471/PDF/RR-1088.pdf},
}
@book{Church:1985,
 author = {A. Church},
 title = {The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies)},
 year = {1985},
} 
@book{CHS:72,
  author = {H. B. Curry and J. R. Hindley and J. P. Seldin},
  title = {Combinatory Logic, Volume II},
  year = {1972},
  pages = {xiv+520}
}

@article{Barendregt:97,
  author    = {H Barendregt},
  title     = {The impact of the lambda calculus in logic and computer
               science},
  journal   = {Bulletin of Symbolic Logic},
  volume    = {3},
  number    = {2},
  year      = {1997},
  pages     = {181-215},
  ee        = {http://www.math.ucla.edu/$\sim$asl/bsl/0302/0302-003.ps},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@dissertation{Girard:72,
author="J.-Y. Girard",
title="Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur",
institution="Universit\'e Paris VII",
year="1972"}

@book{Girard:1989,
 author = {J.-Y. Girard and P. Taylor and Y. Lafont},
 title = {Proofs and types},
 year = {1989},
 isbn = {0-521-37181-3},
 address = {New York, NY, USA},
} 

@inproceedings{Werner:92,
author = {B. Werner},
title = {{A Normalization Proof for an Impredicative Type System with Large Elimination over Integers}},
booktitle="International Workshop on Types for Proofs and Programs (TYPES)",
year="1992",
editor={B. Nordstr\"om and K. Petersson and G. Plotkin},
pages="341--357",
}
@article{Coquand:1988,
 author = {T. Coquand and G. Huet},
 title = {The calculus of constructions},
 journal = {Inf. Comput.},
 issue_date = {February/March 1988},
 volume = {76},
 number = {2-3},
 month = feb,
 year = {1988},
 pages = {95--120},
} 
@incollection{Paulin:1993,
  title={Inductive definitions in the system coq rules and properties},
  author={C. Paulin-Mohring},
  booktitle={Typed lambda calculi and applications},
  pages={328--345},
  year={1993},
}
@article{Jansen:2011,
  author    = {J.M. Jansen and R. Plasmeijer and P. Koopman},
  title     = {Functional Pearl: Comprehensive Encoding of Data Types and Algorithms in the lambda-Calculus},
  journal   = {Internal report, NLDA},
  year      = {2011},
}
@phdthesis{miquel:2001,
  title={Le Calcul des Constructions implicite: syntaxe et s{\'e}mantique},
  author={A. Miquel},
  year={2001},
  school={PhD thesis, Universit{\'e} Paris 7}
}
@incollection{ahn:2013,
  title={System {Fi}},
  author={K.Y. Ahn and T. Sheard and M. Fiore and A.M. Pitts},
  booktitle={Typed Lambda Calculi and Applications},
  pages={15--30},
  year={2013},
}

@article{Hardin:1989,
 author = {T. Hardin},
 title = {Confluence results for the pure strong categorical logic CCL. $\lambda$-calculi as subsystems of CCL},
 journal = {Theoretical Computer Science},
 volume = {65},
 number = {3},
 month = jul,
 year = {1989},
 pages = {291--342},
} 
@article{Rosen:1973,
 author = {B. Rosen},
 title = {Tree-Manipulating Systems and Church-Rosser Theorems},
 journal = {J. ACM},
 volume = {20},
 number = {1},
 year = {1973},
 pages = {160--187},
} 
@phdthesis{hindley1964,
  title={The Church-Rosser property and a result in combinatory logic.},
  author={J. Hindley},
  year={1964},
  school={University of Newcastle upon Tyne}
}

@inproceedings{kuan2007,
  title={A rewriting semantics for type inference},
  author={G. Kuan and D. MacQueen and R. Findler},
  booktitle={Proceedings of the 16th European Symposium on Programming},
  pages={426--440},
  year={2007},
}

@inproceedings{stump2011,
  title={Type Preservation as a Confluence Problem.},
  author={A. Stump and G. Kimmell and R. Omar},
  booktitle={Rewriting Techniques and Applications},
  pages={345--360},
  year={2011}
}

@manuscript{fu+14,
author={P. Fu and A. Stump},
title={{Self Types for Dependently Typed Lambda Encodings}},
note="Extended version available from \url{http://homepage.cs.uiowa.edu/~pfu/document/papers/rta-tlca.pdf}",
year=2014}

@misc{barendregt:1993,
  title={Lambda calculi with types, Handbook of logic in computer science (vol. 2): background: computational structures},
  author={H. Barendregt},
  year={1993},
}

@article{Ariola:1997,
title = "Lambda Calculus with Explicit Recursion ",
journal = "Information and Computation ",
volume = "139",
number = "2",
pages = "154 -- 233",
year = "1997",
author = "Z. Ariola and J. Klop"
}

@book{Barendregt:1985,
  title={The lambda calculus: Its syntax and semantics},
  author={H. Barendregt},
  year={1985},
}



@article{barras10,
	author = {B. Barras},
	title = {Sets in Coq, Coq in Sets},
	journal = {Journal of Formalized Reasoning},
	volume = {3},
	number = {1},
	year = {2010}
}

@phdthesis{werner:phd,
  author = "B. Werner",
  title = "Une th\'{e}orie des constructions inductives",
  school = "Universit\'{e} Paris VII",
  year = 1994,
}

@PHDTHESIS{gimenez96,
url = "http://www.theses.fr/1996ENSL0044",
title = "Un calcul de constructions infinies et son application a la verification de systemes communicants",
author = "E. Gimenez",
year = "1996",
}


@inproceedings{abel+13,
  author    = {A. Abel and
               B. Pientka},
  title     = {Wellfounded recursion with copatterns: a unified approach
               to termination and productivity},
  year      = {2013},
  pages     = {185--196},
  editor    = {G. Morrisett and
               T. Uustalu},
  booktitle     = {International Conference on Functional Programming (ICFP)},
}

@article{capretta05,
  author    = {V. Capretta},
  title     = {General recursion via coinductive types},
  journal   = {Logical Methods in Computer Science},
  volume    = {1},
  number    = {2},
  year      = {2005},
}

@misc{schepler13,
author = {D. Schepler},
title = "bijective function implies equal types is provably inconsistent with functional extensionality in Coq",
note = "message to the Coq Club mailing list, December 12, 2013"}

@inproceedings{geuvers94,                  
title = {{Inductive and Coinductive Types with Iteration and Recursion}},
author = "H. Geuvers",
year = 1994,
booktitle="Informal proceedings of the 1992 workshop on Types for Proofs and Programs",
editor="B. Nordstrom and K. Petersson and G. Plotkin",
pages="183--207"}.

@inproceedings{geuvers01,
  author    = {H. Geuvers},
  title     = {{Induction Is Not Derivable in Second Order Dependent Type
               Theory}},
  booktitle = {Typed Lambda Calculi and Applications (TLCA)},
  year      = {2001},
  pages     = {166-181},
}

@inproceedings{parigot88,
  author    = {M. Parigot},
  title     = {{Programming with Proofs: A Second Order Type Theory}},
  year      = {1988},
  pages     = {145-159},
  editor    = {H. Ganzinger},
  booktitle     = {Proceedings of the 2nd European Symposium on Programming (ESOP)},
}
                  
@inproceedings{altenkirch+10,
  author    = {T. Altenkirch and
               N. Danielsson and
               A. L{\"o}h and
               N. Oury},
  title     = {PiSigma: Dependent Types without the Sugar},
  year      = {2010},
  pages     = {40-55},
  editor    = {M. Blume and
               N. Kobayashi and
               G. Vidal},
  booktitle     = {10th International Symposium on Functional and Logic Programming (FLOPS)},
}

@INPROCEEDINGS{hickey96,
    author = {J. Hickey},
    title = {Formal Objects in Type Theory Using Very Dependent Types},
    editor={K. Bruce} ,                 
    booktitle = {In Foundations of Object Oriented Languages (FOOL) 3},
    year = {1996}
}

@inproceedings{odersky+03,
  author    = {M. Odersky and
               V. Cremet and
               C. R{\"o}ckl and
               M. Zenger},
  title     = {{A Nominal Theory of Objects with Dependent Types}},
  booktitle = {17th European Conference on Object-Oriented Programming
                  (ECOOP)},
  year      = {2003},
  pages     = {201-224},
  editor    = {L. Cardelli},
}

@TECHREPORT{crary99,
    author = {K. Crary},
    title = {{Simple, Efficient Object Encoding using Intersection Types}},
    institution = {Carnegie Mellon University},
    number={CMU-CS-99-100},
    year = {1999}
}

@INPROCEEDINGS{abadi+94,
    author = {M. Abadi and L. Cardelli},
    title = {{A Theory of Primitive Objects - Second-Order Systems}},
    booktitle = {European Symposium on Programming (ESOP)},
    year = {1994},
    pages = {1--25},
}
